package typechecker.walkers;

import java.util.List;
import java.util.Vector;

import typechecker.Stage;
import typechecker.TypeCheckingException;
import typechecker.ast.type.ForallType;
import typechecker.ast.type.FunctionType;
import typechecker.ast.type.TypeConstructor;
import typechecker.ast.type.TypeConstructorApplication;
import typechecker.ast.type.TypeExpression;
import typechecker.ast.type.TypeVariable;

/**
 * Checks if the type of a constructor satisfies the following properties
 * 	- The type constructor 'd' appears only on positive positions
 *  - Any argument of 'd' should appear only on positive positions
 *  - 'd' appears only applied to the same parameters as in the declaration
 */
public class PositivityChecker {
	/* The constructor name and it's params */
	private TypeConstructor cons;
	private List<TypeVariable> paramsList = new Vector<TypeVariable>();
	private Stage st;
	
	public PositivityChecker(TypeConstructor name, List<TypeVariable> params, String baseVar) {
		this.cons = name;
		this.paramsList.addAll(params);
		this.st = new Stage(baseVar, 0);
	}
	
	public boolean checkPositivityConstructorApplication(TypeConstructorApplication tca, boolean positive) {
		TypeConstructor tc = tca.getCons();
		Vector<TypeVariable> actualParams = new Vector<TypeVariable>();
		
		if(!tc.equals(cons)){
			return true;
		}
		
		/* Every occurence of the type constructor in arguments has same stage */ 
		tc.setStage(st);
		
		/* Every occurence of the current type constructor must have same params */
		for( TypeExpression te : tca.getParams()){
			if( !(te instanceof TypeVariable))
				return false;
			actualParams.add(((TypeVariable)te));
		}
		if(!actualParams.equals(paramsList)){
			throw new TypeCheckingException("Type constructor "+ tc.preetyPrint() + " defined with params " + paramsList + " and used with " + actualParams);
		}
		
		/* The constructor must appear at positive position */
		return positive;
	}

	public boolean checkPositivityForallType(ForallType ft, boolean positive) {
		return checkPositivity(ft.getBody(), positive);
	}

	public boolean checkPositivityFunctionType(FunctionType ft, boolean positive) {
		return checkPositivity(ft.getSrc(), !positive) && checkPositivity(ft.getDest(), positive);
	}

	public boolean checkPositivityVariable(TypeVariable tv, boolean positive) {
		/* Any parameter should appear on positive positions */
		if(paramsList.contains(tv))	
			return positive;
		return true;
	}
	
	public boolean checkPositivity(TypeExpression te, boolean param){
		if (te instanceof ForallType){
			return checkPositivityForallType((ForallType)te, param);
		} else if ( te instanceof FunctionType){
			return checkPositivityFunctionType((FunctionType)te, param);
		} else if ( te instanceof TypeConstructorApplication){
			return checkPositivityConstructorApplication((TypeConstructorApplication) te, param);
		} else if ( te instanceof TypeVariable){
			return checkPositivityVariable((TypeVariable)te, param);
		}
		return false;
	}
}
